From: Stefano Zacchiroli Date: Sat, 4 Jun 2005 17:23:42 +0000 (+0000) Subject: snapshot (first version with working pattern matching both 3->2 and 2->1) X-Git-Tag: PRE_INDEX_1~69 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bf6144a808a16d4e576e56593bbcd63b8db5fe4c;p=helm.git snapshot (first version with working pattern matching both 3->2 and 2->1) yupppppieeeeeeeeeeeeeeeeee! yayyyy --- diff --git a/helm/ocaml/cic_notation/.depend b/helm/ocaml/cic_notation/.depend index 980ae1260..cd8873184 100644 --- a/helm/ocaml/cic_notation/.depend +++ b/helm/ocaml/cic_notation/.depend @@ -17,11 +17,9 @@ cicNotationEnv.cmx: cicNotationPt.cmx cicNotationEnv.cmi cicNotationPp.cmo: cicNotationPt.cmo cicNotationEnv.cmi cicNotationPp.cmi cicNotationPp.cmx: cicNotationPt.cmx cicNotationEnv.cmx cicNotationPp.cmi cicNotationMatcher.cmo: cicNotationUtil.cmi cicNotationTag.cmi \ - cicNotationPt.cmo cicNotationPp.cmi cicNotationEnv.cmi \ - cicNotationMatcher.cmi + cicNotationPt.cmo cicNotationEnv.cmi cicNotationMatcher.cmi cicNotationMatcher.cmx: cicNotationUtil.cmx cicNotationTag.cmx \ - cicNotationPt.cmx cicNotationPp.cmx cicNotationEnv.cmx \ - cicNotationMatcher.cmi + cicNotationPt.cmx cicNotationEnv.cmx cicNotationMatcher.cmi cicNotationFwd.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationEnv.cmi \ cicNotationFwd.cmi cicNotationFwd.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationEnv.cmx \ diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index 8da7a483d..f8f73e66b 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -34,28 +34,34 @@ type pattern_id = int exception No_match module OrderedInt = - struct +struct type t = int let compare (x1:t) (x2:t) = Pervasives.compare x2 x1 (* reverse order *) - end +end module IntSet = Set.Make (OrderedInt) let int_set_of_int_list l = List.fold_left (fun acc i -> IntSet.add i acc) IntSet.empty l +type pattern_kind = Variable | Constructor +type tag_t = int + module type PATTERN = - sig +sig type pattern_t - val compatible : pattern_t -> pattern_t -> bool - end + type term_t + val classify : pattern_t -> pattern_kind + val tag_of_pattern : pattern_t -> tag_t * pattern_t list + val tag_of_term : term_t -> tag_t * term_t list +end -module Patterns (P: PATTERN) = - struct +module Matcher (P: PATTERN) = +struct type row_t = P.pattern_t list * P.pattern_t list * pattern_id type t = row_t list - let empty = [] + let compatible p1 p2 = P.classify p1 = P.classify p2 let matched = List.map (fun (matched, _, pid) -> matched, pid) @@ -82,21 +88,22 @@ module Patterns (P: PATTERN) = (* return 2 lists of rows, first one containing homogeneous rows according * to "compatible" below *) let horizontal_split t = - let ap, first_row, t' = + let ap, first_row, t', first_row_class = match t with | [] -> assert false | (_, [], _) :: _ -> assert false (* are_empty should have been invoked in advance *) - | ((_, hd :: _ , _) as row) :: tl -> hd, row, tl + | ((_, hd :: _ , _) as row) :: tl -> hd, row, tl, P.classify hd in let rec aux prev_t = function | [] -> List.rev prev_t, [] | (_, [], _) :: _ -> assert false - | ((_, hd :: _, _) as row) :: tl when P.compatible ap hd -> + | ((_, hd :: _, _) as row) :: tl when compatible ap hd -> aux (row :: prev_t) tl | t -> List.rev prev_t, t in - aux [first_row] t' + let rows1, rows2 = aux [first_row] t' in + first_row_class, rows1, rows2 (* return 2 lists, first one representing first column, second one * representing a new pattern matrix where matched patterns have been moved @@ -107,227 +114,253 @@ module Patterns (P: PATTERN) = | decls, hd :: tl, pid -> hd :: decls, tl, pid | _ -> assert false) t + + let variable_closure k = + (fun matched_terms terms -> + prerr_endline "variable_closure"; + match terms with + | hd :: tl -> k (hd :: matched_terms) tl + | _ -> assert false) + + let constructor_closure ks k = + (fun matched_terms terms -> + prerr_endline "constructor_closure"; + match terms with + | t :: tl -> + (try + let tag, subterms = P.tag_of_term t in + let k' = List.assoc tag ks in + k' matched_terms (subterms @ tl) + with Not_found -> k matched_terms terms) + | [] -> assert false) + + let compiler rows match_cb fail_k = + let rec aux t k = + if t = [] then + k + else if are_empty t then + let res = match_cb (matched t) in + (fun matched_terms _ -> res matched_terms) + else + match horizontal_split t with + | _, [], _ -> assert false + | Variable, t', [] -> variable_closure (aux (vertical_split t') k) + | Constructor, t', [] -> + let tagl = + List.map + (function + | _, p :: _, _ -> fst (P.tag_of_pattern p) + | _ -> assert false) + t' + in + let clusters = partition t' tagl in + let ks = + List.map + (fun (tag, cluster) -> + let cluster' = + List.map (* add args as patterns heads *) + (function + | matched_p, p :: tl, pid -> + let _, subpatterns = P.tag_of_pattern p in + matched_p, subpatterns @ tl, pid + | _ -> assert false) + cluster + in + tag, aux cluster' k) + clusters + in + constructor_closure ks k + | _, t', t'' -> aux t' (aux t'' k) + in + let t = List.map (fun (p, pid) -> [], [p], pid) rows in + let matcher = aux t (fun _ _ -> fail_k ()) in + (fun term -> matcher [] [term]) +end + +module Matcher21 = +struct + module Pattern21 = + struct + type pattern_t = Pt.term + type term_t = Pt.term + let classify = function + | Pt.Variable _ -> Variable + | Pt.Magic _ + | Pt.Layout _ + | Pt.Literal _ -> assert false + | _ -> Constructor + let tag_of_pattern = CicNotationTag.get_tag + let tag_of_term = CicNotationTag.get_tag end -module T21 = + module M = Matcher (Pattern21) + + let extract_magic term = + let magic_map = ref [] in + let add_magic m = + let name = Util.fresh_name () in + magic_map := (name, m) :: !magic_map; + Pt.Variable (Pt.TermVar name) + in + let rec aux = function + | Pt.AttributedTerm (_, t) -> aux t + | Pt.Literal _ + | Pt.Layout _ -> assert false + | Pt.Variable v -> Pt.Variable v + | Pt.Magic m -> add_magic m + | t -> Util.visit_ast aux t + in + let term' = aux term in + term', !magic_map + + let env_of_matched pl tl = + List.map2 + (fun p t -> + match p, t with + Pt.Variable (Pt.TermVar name), _ -> + name, (Env.TermType, Env.TermValue t) + | Pt.Variable (Pt.NumVar name), (Pt.Num (s, _)) -> + name, (Env.NumType, Env.NumValue s) + | Pt.Variable (Pt.IdentVar name), (Pt.Ident (s, None)) -> + name, (Env.StringType, Env.StringValue s) + | _ -> 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 + (List.map + (fun (p, pid) -> + let p', map = extract_magic p in + (p', pid), (pid, map)) + rows) + in + let magichecker map = + List.fold_left + (fun f (name, m) -> + let m_checker = compile_magic m in + (fun env -> + match m_checker (Env.lookup_term env name) env with + | None -> None + | Some env' -> f env')) + (fun env -> Some env) + map + in + let magichooser candidates = + List.fold_left + (fun f (pid, pl, checker) -> + (fun matched_terms -> + let env = env_of_matched pl matched_terms in + match checker env with + | None -> f matched_terms + | Some env -> Some (env, pid))) + (fun _ -> None) + candidates + in + let match_cb rows = + prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows)); + let candidates = + List.map + (fun (pl, pid) -> + let magic_map = + try List.assoc pid magic_maps with Not_found -> assert false + in + pid, pl, magichecker magic_map) + rows + in + magichooser candidates + in + 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 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 + (fun term env -> + let rec aux term = + match compiled term with + | None -> None + | Some (env', 0) -> Some (env', []) + | Some (env', 1) -> + begin + let acc = Env.lookup_term env' acc_name in + let env'' = Env.remove env' acc_name in + match aux acc with + | None -> None + | Some (base_env, rec_envl) -> + Some (base_env, env'' :: rec_envl ) + end + | _ -> assert false + in + match aux term with + | None -> None + | Some (base_env, rec_envl) -> + Some (base_env @ Env.coalesce_env p_rec_decls rec_envl)) + | _ -> assert false +end + +module Matcher32 = struct + module Pattern32 = + struct + type cic_mask_t = + Blob + | Uri of string + | Appl of cic_mask_t list + + let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t) + + let mask_of_cic = function + | Cic.AAppl (_, tl) -> Appl (List.map (fun _ -> Blob) tl), tl + | Cic.AConst (_, _, []) + | Cic.AVar (_, _, []) + | Cic.AMutInd (_, _, _, []) + | Cic.AMutConstruct (_, _, _, _, []) as t -> Uri (uri_of_term t), [] + | _ -> Blob, [] -module P = Patterns (CicNotationTag) - -(* let return_closure matched = - (fun matched_terms terms -> - prerr_endline "T21.return_closure"; - match terms with - | [] -> matched_terms, matched - | _ -> assert false) *) - -let variable_closure k = - (fun matched_terms terms -> - prerr_endline "T21.variable_closure"; - match terms with - | hd :: tl -> - prerr_endline (sprintf "binding: %s" (CicNotationPp.pp_term hd)); - k (hd :: matched_terms) tl - | _ -> assert false) - -let constructor_closure ks k = - (fun matched_terms terms -> - prerr_endline "T21.constructor_closure"; - match terms with - | t :: tl -> - prerr_endline (sprintf "on term %s" (CicNotationPp.pp_term t)); - (try - let tag, subterms = CicNotationTag.get_tag t in - let k' = List.assoc tag ks in - k' matched_terms (subterms @ tl) - with Not_found -> k matched_terms terms) - | [] -> assert false) - -(* let fold_closure kind p_names names matcher success_k k = - let acc_name = try List.hd names with Failure _ -> assert false in -|+ List.iter (fun (name, _) -> Printf.printf "/// %s\n" name) p_names ; +| - (fun matched_terms terms -> - prerr_endline "T21.fold_closure"; - (match terms with - | t :: tl -> - let rec aux t = - prerr_endline "PORCA TORCIA SONO IN AUX" ; - match matcher t with - | _, [] -> None - | matched_terms, [matched_p, 0] -> Some (matched_terms, []) - | matched_terms, [matched_p, 1] -> - let acc = CicNotationEnv.lookup_term env acc_name in - let env = CicNotationEnv.remove env acc_name in - (match aux acc with - | None -> None - | Some env' -> Some (env :: env')) - | envl -> - List.iter - (fun (env, pid) -> - Printf.printf "*** %s %d\n" (CicNotationPp.pp_env env) pid) - envl ; - flush stdout ; - assert false |+ overlapping patterns, to be handled ... +| + let tag_of_term t = + let mask, tl = mask_of_cic t in + Hashtbl.hash mask, tl + + let mask_of_appl_pattern = function + | Pt.UriPattern s -> Uri s, [] + | Pt.VarPattern _ -> Blob, [] + | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl + + let tag_of_pattern p = + let mask, pl = mask_of_appl_pattern p in + Hashtbl.hash mask, pl + + type pattern_t = Pt.cic_appl_pattern + type term_t = Cic.annterm + + let classify = function + | Pt.VarPattern _ -> Variable + | _ -> Constructor + end + + module M = Matcher (Pattern32) + + let compiler rows = + let match_cb rows = + prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows)); + let pl, pid = try List.hd rows with Not_found -> assert false in + (fun matched_terms -> + let env = + List.map2 + (fun p t -> + match p with + | Pt.VarPattern name -> name, t + | _ -> assert false) + pl matched_terms in - (match aux t with - | None -> k terms envl - | Some env -> - let magic_env = CicNotationEnv.coalesce_env p_names env in - List.map (fun (env, pid) -> magic_env @ env, pid) envl) - | [] -> assert false)) *) - -let compiler0 rows match_cb fail_k = - let rec aux t k = - if t = [] then - k - else if P.are_empty t then - match_cb (P.matched t) - else - match P.horizontal_split t with - | t', [] -> - (match t' with - | [] - | (_, [], _) :: _ -> assert false - | (_, Pt.Variable _ :: _, _) :: _ -> - variable_closure (aux (P.vertical_split t') k) - | _ -> - let tagl = - List.map - (function - | _, p :: _, _ -> fst (CicNotationTag.get_tag p) - | _ -> assert false) - t' - in - let clusters = P.partition t' tagl in - let ks = - List.map - (fun (tag, cluster) -> - let cluster' = - List.map (* add args as patterns heads *) - (function - | matched_p, p :: tl, pid -> - let _, subpatterns = CicNotationTag.get_tag p in - matched_p, subpatterns @ tl, pid - | _ -> assert false) - cluster - in - tag, aux cluster' k) - clusters - in - constructor_closure ks k) - | t', tl -> aux t' (aux tl k) - in - let t = List.map (fun (p, pid) -> [], [p], pid) rows in - let matcher = aux t (fun _ _ -> fail_k ()) in - (fun term -> matcher [] [term]) - -let extract_magic term = - let magic_map = ref [] in - let add_magic m = - let name = Util.fresh_name () in - magic_map := (name, m) :: !magic_map; - Pt.Variable (Pt.TermVar name) - in - let rec aux = function - | Pt.AttributedTerm (_, t) -> aux t - | Pt.Literal _ - | Pt.Layout _ -> assert false - | Pt.Variable v -> Pt.Variable v - | Pt.Magic m -> add_magic m - | t -> Util.visit_ast aux t - in - let term' = aux term in - term', !magic_map - -let env_of_matched pl tl = - List.map2 - (fun p t -> - match p, t with - Pt.Variable (Pt.TermVar name), _ -> - name, (Env.TermType, Env.TermValue t) - | Pt.Variable (Pt.NumVar name), (Pt.Num (s, _)) -> - name, (Env.NumType, Env.NumValue s) - | Pt.Variable (Pt.IdentVar name), (Pt.Ident (s, None)) -> - name, (Env.StringType, Env.StringValue s) - | _ -> 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 - (List.map - (fun (p, pid) -> - let p', map = extract_magic p in - (p', pid), (pid, map)) - rows) - in - let magichecker map = - List.fold_left - (fun f (name, m) -> - let m_checker = compile_magic m in - (fun env -> - match m_checker (Env.lookup_term env name) env with - | None -> None - | Some env' -> f env')) - (fun env -> Some env) - map - in - let magichooser candidates = - List.fold_left - (fun f (pid, pl, checker) -> - (fun matched_terms -> - let env = env_of_matched pl matched_terms in - match checker env with - | None -> f matched_terms - | Some env -> Some (env, pid))) - (fun _ -> None) - candidates - in - let match_cb rows = - prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows)); - let candidates = - List.map - (fun (pl, pid) -> - let magic_map = - try List.assoc pid magic_maps with Not_found -> assert false - in - pid, pl, magichecker magic_map) - rows + Some (env, pid)) in - (fun matched_terms _ -> magichooser candidates matched_terms) - in - compiler0 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 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 - (fun term env -> - let rec aux term = - match compiled term with - | None -> None - | Some (env', 0) -> Some (env', []) - | Some (env', 1) -> - begin - let acc = Env.lookup_term env' acc_name in - let env'' = Env.remove env' acc_name in - match aux acc with - | None -> None - | Some (base_env, rec_envl) -> - Some (base_env, env'' :: rec_envl ) - end - | _ -> assert false - in - match aux term with - | None -> None - | Some (base_env, rec_envl) -> - Some (base_env @ Env.coalesce_env p_rec_decls rec_envl)) - | _ -> assert false - + M.compiler rows match_cb (fun () -> None) end diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.mli b/helm/ocaml/cic_notation/cicNotationMatcher.mli index e999b3c6a..55de82999 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.mli +++ b/helm/ocaml/cic_notation/cicNotationMatcher.mli @@ -23,10 +23,37 @@ * http://helm.cs.unibo.it/ *) -module T21 : - sig - val compiler : - (CicNotationPt.term * int) list -> +type pattern_kind = Variable | Constructor +type tag_t = int + +module type PATTERN = +sig + type pattern_t + type term_t + val classify : pattern_t -> pattern_kind + val tag_of_pattern : pattern_t -> tag_t * pattern_t list + val tag_of_term : term_t -> tag_t * term_t list +end + +module Matcher (P: PATTERN) : +sig + val compiler: + (P.pattern_t * int) list -> + ((P.pattern_t list * int) list -> P.term_t list -> 'a) -> + (unit -> 'a) -> + (P.term_t -> 'a) +end + +module Matcher21: +sig + val compiler : + (CicNotationPt.term * int) list -> (CicNotationPt.term -> (CicNotationEnv.t * int) option) - end +end +module Matcher32: +sig + val compiler : + (CicNotationPt.cic_appl_pattern * int) list -> + (Cic.annterm -> ((string * Cic.annterm) list * int) option) +end diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index ea66d6af4..246417d77 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -525,15 +525,15 @@ EXTEND (* }}} *) (* {{{ Grammar for interpretation, notation level 3 *) argument: [ - [ id = IDENT -> IdentArg id - | SYMBOL <:unicode> (* η *); SYMBOL "."; a = SELF -> EtaArg (None, a) - | SYMBOL <:unicode> (* η *); id = IDENT; SYMBOL "."; a = SELF -> - EtaArg (Some id, a) + [ id = IDENT -> IdentArg (0, id) + | l = LIST1 [ SYMBOL <:unicode> (* η *) -> () ] SEP SYMBOL "."; + SYMBOL "."; id = IDENT -> + IdentArg (List.length l, id) ] ]; level3_term: [ [ u = URI -> UriPattern u - | a = argument -> ArgPattern a + | id = IDENT -> VarPattern id | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" -> (match terms with | [] -> assert false diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index b8fdcfac6..d1a54bcf2 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -129,12 +129,11 @@ and pattern_variable = | FreshVar of string type argument_pattern = - | IdentArg of string - | EtaArg of string option * argument_pattern (* eta abstraction *) + | IdentArg of int * string (* eta-depth, name *) type cic_appl_pattern = | UriPattern of string - | ArgPattern of argument_pattern + | VarPattern of string | ApplPattern of cic_appl_pattern list type phrase = (* TODO hackish: replace with TacticAst.statement or similar *) diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index ec385efce..2e2d8c9d4 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -36,21 +36,6 @@ type term_info = let warning s = prerr_endline ("CicNotation WARNING: " ^ s) -(* module Pattern32 = - struct - type pattern_t = CicNotationPt.cic_appl_pattern - let compatible ap1 ap2 = - match ap1, ap2 with - | CicNotationPt.UriPattern _, CicNotationPt.UriPattern _ - | CicNotationPt.ArgPattern _, CicNotationPt.ArgPattern _ - | CicNotationPt.ApplPattern _, CicNotationPt.ApplPattern _ -> true - | _ -> false - end - -module Patterns32 = Patterns (Pattern32) *) - - (* acic -> ast auxiliary function s *) - let get_types uri = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with @@ -212,208 +197,29 @@ let ast_of_acic0 term_info acic k = (* persistent state *) let level1_patterns21 = Hashtbl.create 211 -(* let level2_patterns32 = Hashtbl.create 211 *) +let level2_patterns32 = Hashtbl.create 211 -let (compiled21: (CicNotationPt.term -> (CicNotationEnv.t * pattern_id) option) +let (compiled21: (CicNotationPt.term -> (CicNotationEnv.t * int) option) +option ref) = + ref None +let (compiled32: (Cic.annterm -> ((string * Cic.annterm) list * int) option) option ref) = ref None -(* let (compiled32: (term_info -> Cic.annterm -> CicNotationPt.term) option ref) = - ref None *) let pattern21_matrix = ref [] -(* let pattern32_matrix = ref Patterns32.empty *) +let pattern32_matrix = ref [] let get_compiled21 () = match !compiled21 with | None -> assert false | Some f -> f -(* let get_compiled32 () = +let get_compiled32 () = match !compiled32 with | None -> assert false - | Some f -> f *) + | Some f -> f let set_compiled21 f = compiled21 := Some f -(* let set_compiled32 f = compiled32 := Some f *) - - (* "envl" is a list of triples: - * , where - * name environment: (string * string) list - * term environment: (string * Cic.annterm) list *) -let return_closure success_k = - (fun term_info terms envl -> -(* prerr_endline "return_closure"; *) - match terms with - | [] -> - (try - success_k term_info (List.hd envl) - with Failure _ -> assert false) - | _ -> assert false) - -let variable_closure names k = - (fun term_info terms envl -> -(* prerr_endline "variable_closure"; *) - match terms with - | hd :: tl -> - let envl' = - List.map2 - (fun arg (name_env, term_env, pid) -> - let rec aux name_env term_env pid arg term = - match arg, term with - Ast.IdentArg name, _ -> - (name_env, (name, term) :: term_env, pid) - | Ast.EtaArg (Some name, arg'), - Cic.ALambda (id, name', ty, body) -> - aux - ((name, (string_of_name name', Some (ty, id))) :: name_env) - term_env pid arg' body - | Ast.EtaArg (Some name, arg'), _ -> - let name' = CicNotationUtil.fresh_name () in - aux ((name, (name', None)) :: name_env) - term_env pid arg' term - | Ast.EtaArg (None, arg'), Cic.ALambda (id, name, ty, body) -> - assert false - | Ast.EtaArg (None, arg'), _ -> - assert false - in - aux name_env term_env pid arg hd) - names envl - in - k term_info tl envl' - | _ -> assert false) - -let appl_closure ks k = - (fun term_info terms envl -> -(* prerr_endline "appl_closure"; *) - (match terms with - | Cic.AAppl (_, args) :: tl -> - (try - let k' = List.assoc (List.length args) ks in - k' term_info (args @ tl) envl - with Not_found -> k term_info terms envl) - | [] -> assert false - | _ -> k term_info terms envl)) - -let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t) - -let uri_closure ks k = - (fun term_info terms envl -> -(* prerr_endline "uri_closure"; *) - (match terms with - | [] -> assert false - | hd :: tl -> -(* prerr_endline (sprintf "uri_of_term = %s" (uri_of_term hd)); *) - begin - try - let k' = List.assoc (uri_of_term hd) ks in - k' term_info tl envl - with - | Invalid_argument _ (* raised by uri_of_term *) - | Not_found -> k term_info terms envl - end)) - - (* compiler from level 3 to level 2 *) -(* let compiler32 (t: Patterns32.t) success_k fail_k = - let rec aux t k = |+ k is a continuation +| - if t = [] then - k - else if Patterns32.are_empty t then begin - (match t with - | _::_::_ -> - |+ XXX optimization possible here: throw away all except one of the - * rules which lead to ambiguity +| - warning "ambiguous interpretation" - | _ -> ()); - return_closure success_k - end else - match Patterns32.horizontal_split t with - | t', [] -> - (match t' with - | [] - | ([], _) :: _ -> assert false - | (Ast.ArgPattern (Ast.IdentArg _) :: _, _) :: _ - | (Ast.ArgPattern (Ast.EtaArg _) :: _, _) :: _ -> - let first_column, t'' = Patterns32.vertical_split t' in - let names = - List.map - (function - | Ast.ArgPattern arg -> arg - | _ -> assert false) - first_column - in - variable_closure names (aux t'' k) - | (Ast.ApplPattern _ :: _, _) :: _ -> - let pidl = - List.map - (function - | (Ast.ApplPattern args) :: _, _ -> List.length args - | _ -> assert false) - t' - in - |+ arity partitioning +| - let clusters = Patterns32.partition t' pidl in - let ks = |+ k continuation list +| - List.map - (fun (len, cluster) -> - let cluster' = - List.map |+ add args as patterns heads +| - (function - | (Ast.ApplPattern args) :: tl, pid -> - |+ let's throw away "teste di cluster" +| - args @ tl, pid - | _ -> assert false) - cluster - in - len, aux cluster' k) - clusters - in - appl_closure ks k - | (Ast.UriPattern _ :: _, _) :: _ -> - let uidmap, pidl = - let urimap = ref [] in - let uidmap = ref [] in - let get_uri_id uri = - try - List.assoc uri !urimap - with - Not_found -> - let uid = List.length !urimap in - urimap := (uri, uid) :: !urimap ; - uidmap := (uid, uri) :: !uidmap ; - uid - in - let uidl = - List.map - (function - | (Ast.UriPattern uri) :: _, _ -> get_uri_id uri - | _ -> assert false) - t' - in - !uidmap, uidl - in - let clusters = Patterns32.partition t' pidl in - let ks = - List.map - (fun (uid, cluster) -> - let cluster' = - List.map - (function - | (Ast.UriPattern uri) :: tl, pid -> tl, pid - | _ -> assert false) - cluster - in - List.assoc uid uidmap, aux cluster' k) - clusters - in - uri_closure ks k) - | t', tl -> aux t' (aux tl k) - in - let matcher = aux t (fun _ _ -> raise No_match) in - (fun term_info annterm -> - try - matcher term_info [annterm] (List.map (fun (_, pid) -> [], [], pid) t) - with No_match -> fail_k term_info annterm) - -let ast_of_acic1 term_info annterm = (get_compiled32 ()) term_info annterm *) +let set_compiled32 f = compiled32 := Some f let instantiate21 env pid = prerr_endline "instantiate21"; @@ -461,63 +267,51 @@ let rec pp_ast1 term = | None -> pp_ast0 term pp_ast1 | Some (env, pid) -> instantiate21 (ast_env_of_env env) pid -(* let instantiate32 term_info name_env term_env pid = - let symbol, args = - try - Hashtbl.find level2_patterns32 pid - with Not_found -> assert false - in +let instantiate32 term_info env symbol args = let rec instantiate_arg = function - | Ast.IdentArg name -> - (try List.assoc name term_env with Not_found -> assert false) - | Ast.EtaArg (None, _) -> assert false |+ TODO +| - | Ast.EtaArg (Some name, arg) -> - let (name', ty_opt) = - try List.assoc name name_env with Not_found -> assert false + | Ast.IdentArg (n, name) -> + let t = (try List.assoc name env with Not_found -> assert false) in + let rec count_lambda = function + | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body + | _ -> 0 in - let body = instantiate_arg arg in - let name' = Ast.Ident (name', None) in - match ty_opt with - | None -> Ast.Binder (`Lambda, (name', None), body) - | Some (ty, id) -> - idref id (Ast.Binder (`Lambda, (name', Some ty), body)) + let rec add_lambda t n = + if n > 0 then + let name = CicNotationUtil.fresh_name () in + Ast.Binder (`Lambda, (Ast.Ident (name, None), None), + Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)]) + else + t + in + add_lambda t (n - count_lambda t) in let args' = List.map instantiate_arg args in Ast.Appl (Ast.Symbol (symbol, 0) :: args') +let rec ast_of_acic1 term_info annterm = + match (get_compiled32 ()) annterm with + | None -> ast_of_acic0 term_info annterm ast_of_acic1 + | Some (env, pid) -> + let env' = + List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env + in + let symbol, args = + try + Hashtbl.find level2_patterns32 pid + with Not_found -> assert false + in + instantiate32 term_info env' symbol args + let load_patterns32 t = - let ast_env_of_name_env term_info name_env = - List.map - (fun (name, (name', ty_opt)) -> - let ast_ty_opt = - match ty_opt with - | None -> None - | Some (annterm, id) -> Some (ast_of_acic1 term_info annterm, id) - in - (name, (name', ast_ty_opt))) - name_env - in - let ast_env_of_term_env term_info = - List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) - in - let fail_k term_info annterm = ast_of_acic0 term_info annterm ast_of_acic1 in - let success_k term_info (name_env, term_env, pid) = - instantiate32 - term_info - (ast_env_of_name_env term_info name_env) - (ast_env_of_term_env term_info term_env) - pid - in - let compiled32 = compiler32 t success_k fail_k in - set_compiled32 compiled32 *) + set_compiled32 (CicNotationMatcher.Matcher32.compiler t) let load_patterns21 t = - set_compiled21 (CicNotationMatcher.T21.compiler t) + set_compiled21 (CicNotationMatcher.Matcher21.compiler t) -(* let ast_of_acic id_to_sort annterm = +let ast_of_acic id_to_sort annterm = let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in let ast = ast_of_acic1 term_info annterm in - ast, term_info.uri *) + ast, term_info.uri let pp_ast term = pp_ast1 term @@ -527,12 +321,12 @@ let fresh_id = incr counter; !counter -(* let add_interpretation (symbol, args) appl_pattern = +let add_interpretation (symbol, args) appl_pattern = let id = fresh_id () in Hashtbl.add level2_patterns32 id (symbol, args); - pattern32_matrix := ([appl_pattern], id) :: !pattern32_matrix; + pattern32_matrix := (appl_pattern, id) :: !pattern32_matrix; load_patterns32 !pattern32_matrix; - id *) + id let add_pretty_printer ?precedence ?associativity l2 l1 = let id = fresh_id () in @@ -545,12 +339,12 @@ let add_pretty_printer ?precedence ?associativity l2 l1 = exception Interpretation_not_found exception Pretty_printer_not_found -(* let remove_interpretation id = +let remove_interpretation id = (try Hashtbl.remove level2_patterns32 id; with Not_found -> raise Interpretation_not_found); pattern32_matrix := List.filter (fun (_, id') -> id <> id') !pattern32_matrix; - load_patterns32 !pattern32_matrix *) + load_patterns32 !pattern32_matrix let remove_pretty_printer id = (try @@ -561,5 +355,5 @@ let remove_pretty_printer id = let _ = load_patterns21 []; -(* load_patterns32 [] *) + load_patterns32 [] diff --git a/helm/ocaml/cic_notation/cicNotationRew.mli b/helm/ocaml/cic_notation/cicNotationRew.mli index a57ddd0de..21877d0c3 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.mli +++ b/helm/ocaml/cic_notation/cicNotationRew.mli @@ -24,22 +24,22 @@ *) (** level 3 -> level 2 *) -(* val ast_of_acic: - (Cic.id, CicNotationPt.sort_kind) Hashtbl.t -> |+ id -> sort +| - Cic.annterm -> |+ acic +| - CicNotationPt.term |+ ast +| - * (Cic.id, string) Hashtbl.t |+ id -> uri +| *) +val ast_of_acic: + (Cic.id, CicNotationPt.sort_kind) Hashtbl.t -> (* id -> sort *) + Cic.annterm -> (* acic *) + CicNotationPt.term (* ast *) + * (Cic.id, string) Hashtbl.t (* id -> uri *) (** level 2 -> level 1 *) val pp_ast: CicNotationPt.term -> CicNotationPt.term -(* type interpretation_id *) +type interpretation_id type pretty_printer_id -(* val add_interpretation: - string * CicNotationPt.argument_pattern list -> |+ level 2 pattern +| - CicNotationPt.cic_appl_pattern -> |+ level 3 pattern +| - interpretation_id *) +val add_interpretation: + string * CicNotationPt.argument_pattern list -> (* level 2 pattern *) + CicNotationPt.cic_appl_pattern -> (* level 3 pattern *) + interpretation_id val add_pretty_printer: ?precedence:int -> @@ -52,7 +52,7 @@ exception Interpretation_not_found exception Pretty_printer_not_found (** @raise Interpretation_not_found *) -(* val remove_interpretation: interpretation_id -> unit *) +val remove_interpretation: interpretation_id -> unit (** @raise Pretty_printer_not_found *) val remove_pretty_printer: pretty_printer_id -> unit diff --git a/helm/ocaml/cic_notation/cicNotationTag.mli b/helm/ocaml/cic_notation/cicNotationTag.mli index 62f9ca091..bf04e0a9f 100644 --- a/helm/ocaml/cic_notation/cicNotationTag.mli +++ b/helm/ocaml/cic_notation/cicNotationTag.mli @@ -23,9 +23,5 @@ * http://helm.cs.unibo.it/ *) -type tag = int -type pattern_t = CicNotationPt.term - -val get_tag: pattern_t -> tag * pattern_t list -val compatible: pattern_t -> pattern_t -> bool +val get_tag: CicNotationPt.term -> int * CicNotationPt.term list diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index 5b42822c2..77135a977 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -103,14 +103,13 @@ let _ = | P.Interpretation (l2, l3) -> print_endline "Adding interpretation ..."; flush stdout; let time1 = Unix.gettimeofday () in -(* ignore (CicNotationRew.add_interpretation l2 l3); *) + ignore (CicNotationRew.add_interpretation l2 l3); let time2 = Unix.gettimeofday () in printf "done (patterns compilation took %f seconds)\n" (time2 -. time1); flush stdout | P.Render uri -> - assert false -(* let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in let annobj, _, _, id_to_sort, _, _, _ = Cic2acic.acic_object_of_cic_object obj in @@ -133,7 +132,7 @@ let _ = let t' = CicNotationRew.pp_ast t in let time4 = Unix.gettimeofday () in printf "pretty printing took %f seconds\n" (time4 -. time3); - print_endline (CicNotationPp.pp_term t'); flush stdout *) + print_endline (CicNotationPp.pp_term t'); flush stdout ) (* CicNotationParser.print_l2_pattern ()) *) | 1 -> ignore (CicNotationParser.parse_syntax_pattern istream)