X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=8bbc22e24344819e37e7758abe8c5dc6f54f8f40;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=e037ca2a97e4b621d2c2b7ac9c663ffe2581b764;hpb=dbcc29c0e46454c7e31b485135900ceab38627e1;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index e037ca2a9..8bbc22e24 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -25,165 +25,20 @@ open Printf +module Ast = CicNotationPt + +let debug = false +let debug_print s = if debug then prerr_endline (Lazy.force s) else () + type pattern_id = int type interpretation_id = pattern_id type pretty_printer_id = pattern_id type term_info = - { sort: (Cic.id, CicNotationPt.sort_kind) Hashtbl.t; - uri: (Cic.id, string) Hashtbl.t; + { sort: (Cic.id, Ast.sort_kind) Hashtbl.t; + uri: (Cic.id, UriManager.uri) Hashtbl.t; } -exception No_match - -module OrderedInt = - struct - type t = int - let compare (x1:t) (x2:t) = Pervasives.compare x2 x1 (* reverse order *) - 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 - -let warning s = prerr_endline ("CicNotation WARNING: " ^ s) - -module type PATTERN = - sig - type pattern_t - val compatible : pattern_t -> pattern_t -> bool - end - -module Patterns (P: PATTERN) = - struct - type row_t = P.pattern_t list * pattern_id - type t = row_t list - - let empty = [] - - let first_column t = List.map (fun (patterns, _) -> List.hd patterns) t - let pattern_ids t = List.map snd t - - let partition t pidl = - let partitions = Hashtbl.create 11 in - let add pid row = Hashtbl.add partitions pid row in - (try - List.iter2 add pidl t - with Invalid_argument _ -> assert false); - let pidset = int_set_of_int_list pidl in - IntSet.fold - (fun pid acc -> - match Hashtbl.find_all partitions pid with - | [] -> acc - | patterns -> (pid, List.rev patterns) :: acc) - pidset [] - - let are_empty t = fst (List.hd t) = [] - (* if first row has an empty list of patterns, then others will as well *) - - (* return 2 lists of rows, first one containing homogeneous rows according - * to "compatible" below *) - let horizontal_split t = - let ap = - match t with - | [] -> assert false - | ([], _) :: _ -> - assert false (* are_empty should have been invoked in advance *) - | (hd :: _ , _) :: _ -> hd - in - let rec aux prev_t = function - | [] -> List.rev prev_t, [] - | ([], _) :: _ -> assert false - | (((hd :: _), _) as row) :: tl when P.compatible ap hd -> - aux (row :: prev_t) tl - | t -> List.rev prev_t, t - in - aux [] t - - (* return 2 lists, first one representing first column, second one - * representing rows stripped of the first element *) - let vertical_split t = - let l = - List.map - (function - | (hd :: tl, pid) -> hd, (tl, pid) - | _ -> assert false) - t - in - List.split l - end - -module Patterns21 = Patterns (CicNotationTag) - -module Patterns32 = - struct - type row_t = CicNotationPt.cic_appl_pattern list * pattern_id - type t = row_t list - - let empty = [] - - let first_column t = List.map (fun (patterns, _) -> List.hd patterns) t - let pattern_ids t = List.map snd t - - let partition t pidl = - let partitions = Hashtbl.create 11 in - let add pid row = Hashtbl.add partitions pid row in - (try - List.iter2 add pidl t - with Invalid_argument _ -> assert false); - let pidset = int_set_of_int_list pidl in - IntSet.fold - (fun pid acc -> - match Hashtbl.find_all partitions pid with - | [] -> acc - | patterns -> (pid, List.rev patterns) :: acc) - pidset [] - - let are_empty t = fst (List.hd t) = [] - (* if first row has an empty list of patterns, then others will as well *) - - (* return 2 lists of rows, first one containing homogeneous rows according - * to "compatible" below *) - let horizontal_split t = - let compatible ap1 ap2 = - match ap1, ap2 with - | CicNotationPt.UriPattern _, CicNotationPt.UriPattern _ - | CicNotationPt.ArgPattern _, CicNotationPt.ArgPattern _ - | CicNotationPt.ApplPattern _, CicNotationPt.ApplPattern _ -> true - | _ -> false - in - let ap = - match t with - | [] -> assert false - | ([], _) :: _ -> - assert false (* are_empty should have been invoked in advance *) - | (hd :: _ , _) :: _ -> hd - in - let rec aux prev_t = function - | [] -> List.rev prev_t, [] - | ([], _) :: _ -> assert false - | (((hd :: _), _) as row) :: tl when compatible ap hd -> - aux (row :: prev_t) tl - | t -> List.rev prev_t, t - in - aux [] t - - (* return 2 lists, first one representing first column, second one - * representing rows stripped of the first element *) - let vertical_split t = - let l = - List.map - (function - | (hd :: tl, pid) -> hd, (tl, pid) - | _ -> assert false) - t - in - List.split l - end - - (* acic -> ast auxiliary function s *) - let get_types uri = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with @@ -209,33 +64,248 @@ let constructor_of_inductive_type uri i j = fst (List.nth (constructors_of_inductive_type uri i) (j-1)) with Not_found -> assert false) -module Ast = CicNotationPt - -let string_of_name = function - | Cic.Name s -> s - | Cic.Anonymous -> "_" - -let ident_of_name n = Ast.Ident (string_of_name n, None) - let idref id t = Ast.AttributedTerm (`IdRef id, t) +let resolve_binder = function + | `Lambda -> "\\lambda" + | `Pi -> "\\Pi" + | `Forall -> "\\forall" + | `Exists -> "\\exists" + +let add_level_info prec assoc t = Ast.AttributedTerm (`Level (prec, assoc), t) +let add_pos_info pos t = Ast.AttributedTerm (`ChildPos pos, t) +let left_pos = add_pos_info `Left +let right_pos = add_pos_info `Right +let inner_pos = add_pos_info `Inner + +let rec top_pos t = add_level_info ~-1 Gramext.NonA (inner_pos t) +(* function + | Ast.AttributedTerm (`Level _, t) -> + add_level_info ~-1 Gramext.NonA (inner_pos t) + | Ast.AttributedTerm (attr, t) -> Ast.AttributedTerm (attr, top_pos t) + | t -> add_level_info ~-1 Gramext.NonA (inner_pos t) *) + +let rec remove_level_info = + function + | Ast.AttributedTerm (`Level _, t) -> remove_level_info t + | Ast.AttributedTerm (a, t) -> Ast.AttributedTerm (a, remove_level_info t) + | t -> t + +let add_xml_attrs attrs t = + if attrs = [] then t else Ast.AttributedTerm (`XmlAttrs attrs, t) + +let add_keyword_attrs = + add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) + +let box kind spacing indent content = + Ast.Layout (Ast.Box ((kind, spacing, indent), content)) + +let hbox = box Ast.H +let vbox = box Ast.V +let hvbox = box Ast.HV +let hovbox = box Ast.HOV +let break = Ast.Layout Ast.Break +let builtin_symbol s = Ast.Literal (`Symbol s) +let keyword k = add_keyword_attrs (Ast.Literal (`Keyword k)) + +let number s = + add_xml_attrs (RenderingAttrs.number_attributes `MathML) + (Ast.Literal (`Number s)) + +let ident i = + add_xml_attrs (RenderingAttrs.ident_attributes `MathML) (Ast.Ident (i, None)) + +let ident_w_href href i = + match href with + | None -> ident i + | Some href -> + let href = UriManager.string_of_uri href in + add_xml_attrs [Some "xlink", "href", href] (ident i) + +let binder_symbol s = + add_xml_attrs (RenderingAttrs.builtin_symbol_attributes `MathML) + (builtin_symbol s) + +let string_of_sort_kind = function + | `Prop -> "Prop" + | `Set -> "Set" + | `CProp -> "CProp" + | `Type _ -> "Type" + let pp_ast0 t k = - prerr_endline "pp_ast0"; - let rec aux t = CicNotationUtil.visit_ast ~special_k k t + let rec aux = + function + | Ast.Appl ts -> + let rec aux_args pos = + function + | [] -> [] + | [ last ] -> + let last = k last in + if pos = `Left then [ left_pos last ] else [ right_pos last ] + | hd :: tl -> + (add_pos_info pos (k hd)) :: aux_args `Inner tl + in + add_level_info Ast.apply_prec Ast.apply_assoc + (hovbox true true (CicNotationUtil.dress break (aux_args `Left ts))) + | Ast.Binder (binder_kind, (id, ty), body) -> + add_level_info Ast.binder_prec Ast.binder_assoc + (hvbox false true + [ binder_symbol (resolve_binder binder_kind); + k id; builtin_symbol ":"; aux_ty ty; break; + builtin_symbol "."; right_pos (k body) ]) + | Ast.Case (what, indty_opt, outty_opt, patterns) -> + let outty_box = + match outty_opt with + | None -> [] + | Some outty -> + [ keyword "return"; break; remove_level_info (k outty)] + in + let indty_box = + match indty_opt with + | None -> [] + | Some (indty, href) -> [ keyword "in"; break; ident_w_href href indty ] + in + let match_box = + hvbox false false [ + hvbox false true [ + hvbox false true [ keyword "match"; break; top_pos (k what) ]; + break; + hvbox false true indty_box; + break; + hvbox false true outty_box + ]; + break; + keyword "with" + ] + in + let mk_case_pattern (head, href, vars) = + hbox true false (ident_w_href href head :: List.map aux_var vars) + in + let patterns' = + List.map + (fun (lhs, rhs) -> + remove_level_info + (hvbox false true [ + hbox false true [ + mk_case_pattern lhs; builtin_symbol "\\Rightarrow" ]; + break; top_pos (k rhs) ])) + patterns + in + let patterns'' = + let rec aux_patterns = function + | [] -> assert false + | [ last ] -> + [ break; + hbox false false [ + builtin_symbol "|"; + last; builtin_symbol "]" ] ] + | hd :: tl -> + [ break; hbox false false [ builtin_symbol "|"; hd ] ] + @ aux_patterns tl + in + match patterns' with + | [] -> + [ hbox false false [ builtin_symbol "["; builtin_symbol "]" ] ] + | [ one ] -> + [ hbox false false [ + builtin_symbol "["; one; builtin_symbol "]" ] ] + | hd :: tl -> + hbox false false [ builtin_symbol "["; hd ] + :: aux_patterns tl + in + add_level_info Ast.simple_prec Ast.simple_assoc + (hvbox false false [ + hvbox false false ([match_box]); break; + hbox false false [ hvbox false false patterns'' ] ]) + | Ast.Cast (bo, ty) -> + add_level_info Ast.simple_prec Ast.simple_assoc + (hvbox false true [ + builtin_symbol "("; top_pos (k bo); break; builtin_symbol ":"; + top_pos (k ty); builtin_symbol ")"]) + | Ast.LetIn (var, s, t) -> + add_level_info Ast.let_in_prec Ast.let_in_assoc + (hvbox false true [ + hvbox false true [ + keyword "let"; + hvbox false true [ + aux_var var; builtin_symbol "\\def"; break; top_pos (k s) ]; + break; keyword "in" ]; + break; + k t ]) + | Ast.LetRec (rec_kind, funs, where) -> + let rec_op = + match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec" + in + let mk_fun (var, body, _) = aux_var var, k body in + let mk_funs = List.map mk_fun in + let fst_fun, tl_funs = + match mk_funs funs with hd :: tl -> hd, tl | [] -> assert false + in + let fst_row = + let (name, body) = fst_fun in + hvbox false true [ + keyword "let"; keyword rec_op; name; builtin_symbol "\\def"; break; + top_pos body ] + in + let tl_rows = + List.map + (fun (name, body) -> + [ break; + hvbox false true [ + keyword "and"; name; builtin_symbol "\\def"; break; body ] ]) + tl_funs + in + add_level_info Ast.let_in_prec Ast.let_in_assoc + ((hvbox false false + (fst_row :: List.flatten tl_rows + @ [ break; keyword "in"; break; k where ]))) + | Ast.Implicit -> builtin_symbol "?" + | Ast.Meta (n, l) -> + let local_context l = + CicNotationUtil.dress (builtin_symbol ";") + (List.map (function None -> builtin_symbol "_" | Some t -> k t) l) + in + hbox false false + ([ builtin_symbol "?"; number (string_of_int n) ] + @ (if l <> [] then local_context l else [])) + | Ast.Sort sort -> aux_sort sort + | Ast.Num _ + | Ast.Symbol _ + | Ast.Ident (_, None) | Ast.Ident (_, Some []) + | Ast.Uri (_, None) | Ast.Uri (_, Some []) + | Ast.Literal _ + | Ast.UserInput as leaf -> leaf + | t -> CicNotationUtil.visit_ast ~special_k k t + and aux_sort sort_kind = + add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) + (Ast.Ident (string_of_sort_kind sort_kind, None)) + and aux_ty = function + | None -> builtin_symbol "?" + | Some ty -> k ty + and aux_var = function + | name, Some ty -> + hvbox false true [ + builtin_symbol "("; name; builtin_symbol ":"; break; k ty; + builtin_symbol ")" ] + | name, None -> name and special_k = function - | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, aux t) - | _ -> assert false + | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t) + | t -> + prerr_endline ("unexpected special: " ^ CicNotationPp.pp_term t); + assert false in aux t let ast_of_acic0 term_info acic k = -(* prerr_endline "ast_of_acic0"; *) let k = k term_info in - let register_uri id uri = Hashtbl.add term_info.uri id uri in + let id_to_uris = term_info.uri in + let register_uri id uri = Hashtbl.add id_to_uris id uri in let sort_of_id id = try Hashtbl.find term_info.sort id - with Not_found -> assert false + with Not_found -> + prerr_endline (sprintf "warning: sort of id %s not found, using Type" id); + `Type (CicUniv.fresh ()) in let aux_substs substs = Some @@ -253,63 +323,75 @@ let ast_of_acic0 term_info acic k = let aux = function | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, None)) | Cic.AVar (id,uri,substs) -> - register_uri id (UriManager.string_of_uri uri); + register_uri id uri; idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs)) | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, aux_context l)) | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop) | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set) - | Cic.ASort (id,Cic.Type _) -> idref id (Ast.Sort `Type) + | Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u)) | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp) - | Cic.AImplicit _ -> assert false + | Cic.AImplicit (id, Some `Hole) -> idref id Ast.UserInput + | Cic.AImplicit (id, _) -> idref id Ast.Implicit | Cic.AProd (id,n,s,t) -> let binder_kind = match sort_of_id id with - | `Set | `Type -> `Pi + | `Set | `Type _ -> `Pi | `Prop | `CProp -> `Forall in - idref id (Ast.Binder (binder_kind, (ident_of_name n, Some (k s)), k t)) - | Cic.ACast (id,v,t) -> - idref id (Ast.Appl [idref id (Ast.Symbol ("cast", 0)); k v; k t]) + idref id (Ast.Binder (binder_kind, + (CicNotationUtil.name_of_cic_name n, Some (k s)), k t)) + | Cic.ACast (id,v,t) -> idref id (Ast.Cast (k v, k t)) | Cic.ALambda (id,n,s,t) -> - idref id (Ast.Binder (`Lambda, (ident_of_name n, Some (k s)), k t)) + idref id (Ast.Binder (`Lambda, + (CicNotationUtil.name_of_cic_name n, Some (k s)), k t)) | Cic.ALetIn (id,n,s,t) -> - idref id (Ast.LetIn ((ident_of_name n, None), k s, k t)) + idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, None), + k s, k t)) | Cic.AAppl (aid,args) -> idref aid (Ast.Appl (List.map k args)) | Cic.AConst (id,uri,substs) -> - register_uri id (UriManager.string_of_uri uri); + register_uri id uri; idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs)) | Cic.AMutInd (id,uri,i,substs) as t -> let name = name_of_inductive_type uri i in let uri_str = UriManager.string_of_uri uri in - let puri_str = - uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" - in - register_uri id puri_str; + let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (i+1) in + register_uri id (UriManager.uri_of_string puri_str); idref id (Ast.Ident (name, aux_substs substs)) | Cic.AMutConstruct (id,uri,i,j,substs) -> let name = constructor_of_inductive_type uri i j in let uri_str = UriManager.string_of_uri uri in let puri_str = sprintf "%s#xpointer(1/%d/%d)" uri_str (i + 1) j in - register_uri id puri_str; + register_uri id (UriManager.uri_of_string puri_str); idref id (Ast.Ident (name, aux_substs substs)) | Cic.AMutCase (id,uri,typeno,ty,te,patterns) -> let name = name_of_inductive_type uri typeno in + let uri_str = UriManager.string_of_uri uri in + let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (typeno+1) in + let ctor_puri j = + UriManager.uri_of_string + (sprintf "%s#xpointer(1/%d/%d)" uri_str (typeno+1) j) + in + let case_indty = name, Some (UriManager.uri_of_string puri_str) in let constructors = constructors_of_inductive_type uri typeno in let rec eat_branch ty pat = match (ty, pat) with | Cic.Prod (_, _, t), Cic.ALambda (_, name, s, t') -> let (cv, rhs) = eat_branch t t' in - (ident_of_name name, Some (k s)) :: cv, rhs + (CicNotationUtil.name_of_cic_name name, Some (k s)) :: cv, rhs | _, _ -> [], k pat in + let j = ref 0 in let patterns = - List.map2 - (fun (name, ty) pat -> - let (capture_variables, rhs) = eat_branch ty pat in - ((name, capture_variables), rhs)) - constructors patterns + try + List.map2 + (fun (name, ty) pat -> + incr j; + let (capture_variables, rhs) = eat_branch ty pat in + ((name, Some (ctor_puri !j), capture_variables), rhs)) + constructors patterns + with Invalid_argument _ -> assert false in - idref id (Ast.Case (k te, Some name, Some (k ty), patterns)) + idref id (Ast.Case (k te, Some case_indty, Some (k ty), patterns)) | Cic.AFix (id, no, funs) -> let defs = List.map @@ -328,7 +410,8 @@ let ast_of_acic0 term_info acic k = | Cic.ACoFix (id, no, funs) -> let defs = List.map - (fun (_, n, ty, bo) -> ((Ast.Ident (n, None), Some (k ty)), k bo, 0)) + (fun (_, n, ty, bo) -> + ((Ast.Ident (n, None), Some (k ty)), k bo, 0)) funs in let name = @@ -346,387 +429,243 @@ let ast_of_acic0 term_info acic k = let level1_patterns21 = Hashtbl.create 211 let level2_patterns32 = Hashtbl.create 211 +let interpretations = Hashtbl.create 211 (* symb -> id list ref *) -let (compiled21: (CicNotationPt.term -> CicNotationPt.term) option ref) = - ref None -let (compiled32: (term_info -> Cic.annterm -> CicNotationPt.term) option ref) = - ref None +let compiled21 = ref None +let compiled32 = ref None -let pattern21_matrix = ref Patterns21.empty -let pattern32_matrix = ref Patterns32.empty +let pattern21_matrix = ref [] +let pattern32_matrix = ref [] let get_compiled21 () = match !compiled21 with | None -> assert false - | Some f -> f + | Some f -> Lazy.force f let get_compiled32 () = match !compiled32 with | None -> assert false - | Some f -> f + | Some f -> Lazy.force 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 +let add_idrefs = + List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) + +let instantiate21 idrefs env l1 = + let rec subst_singleton pos env = + function + Ast.AttributedTerm (attr, t) -> + Ast.AttributedTerm (attr, subst_singleton pos env t) + | t -> CicNotationUtil.group (subst pos env t) + and subst pos env = function + | Ast.AttributedTerm (attr, t) as term -> +(* prerr_endline ("loosing attribute " ^ CicNotationPp.pp_attribute attr); *) + subst pos env t + | Ast.Variable var -> + let name, expected_ty = CicNotationEnv.declaration_of_var var in + let ty, value = 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 return_closure21 success_k = - (fun terms envl -> - prerr_endline "return_closure21"; - match terms with - | [] -> - (try - success_k (List.hd envl) - with Failure _ -> assert false) - | _ -> assert false) - -let variable_closure21 vars k = - (fun terms envl -> - prerr_endline "variable_closure21"; - match terms with + List.assoc name env + with Not_found -> + prerr_endline ("name " ^ name ^ " not found in environment"); + assert false + in + assert (CicNotationEnv.well_typed ty value); (* INVARIANT *) + (* following assertion should be a conditional that makes this + * instantiation fail *) + assert (CicNotationEnv.well_typed expected_ty value); + [ add_pos_info pos (CicNotationEnv.term_of_value value) ] + | Ast.Magic m -> subst_magic pos env m + | Ast.Literal l as t -> + let t = add_idrefs idrefs t in + (match l with + | `Keyword k -> [ add_keyword_attrs t ] + | _ -> [ t ]) + | Ast.Layout l -> [ Ast.Layout (subst_layout pos env l) ] + | t -> [ CicNotationUtil.visit_ast (subst_singleton pos env) t ] + and subst_magic pos 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 -> [ Ast.Literal l ] + in + let rec instantiate_list acc = function + | [] -> List.rev acc + | value_set :: [] -> + let env = CicNotationEnv.combine rec_decls value_set in + instantiate_list (CicNotationUtil.group (subst pos env p) :: acc) + [] + | value_set :: tl -> + let env = CicNotationEnv.combine rec_decls value_set in + let terms = subst pos env p in + instantiate_list (CicNotationUtil.group (terms @ sep) :: acc) tl + in + instantiate_list [] values + | 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 + begin + match env with + | [] -> [] + | _ -> subst pos env p + end + | _ -> assert false (* impossible *) + and subst_layout pos env = function + | Ast.Box (kind, tl) -> + let tl' = subst_children pos env tl in + Ast.Box (kind, List.concat tl') + | l -> CicNotationUtil.visit_layout (subst_singleton pos env) l + and subst_children pos env = + function + | [] -> [] + | [ child ] -> + let pos' = + match pos with + | `Inner -> `Right + | `Left -> `Left +(* | `None -> assert false *) + | `Right -> `Right + in + [ subst pos' env child ] | hd :: tl -> - let envl' = - List.map2 (fun var (env, pid) -> (var, hd) :: env, pid) vars envl + let pos' = + match pos with + | `Inner -> `Inner + | `Left -> `Inner +(* | `None -> assert false *) + | `Right -> `Right in - k tl envl' - | _ -> assert false) - -let constructor_closure21 ks k = - (fun terms envl -> - prerr_endline "constructor_closure21"; - (match terms with - | p :: tl -> - prerr_endline (sprintf "on term %s" (CicNotationPp.pp_term p)); - (try - let tag, subterms = CicNotationTag.get_tag p in - let k' = List.assoc tag ks in - k' (subterms @ tl) envl - with Not_found -> k terms envl) - | [] -> assert false)) - -let compiler21 (t: Patterns21.t) success_k fail_k = - let rec aux t k = - if t = [] then - k - else if Patterns21.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 notation" - | _ -> ()); - return_closure21 success_k - end else - match Patterns21.horizontal_split t with - | t', [] -> - (match t' with - | [] - | ([], _) :: _ -> assert false - | (Ast.Variable _ :: _, _) :: _ -> - let first_column, t'' = Patterns21.vertical_split t' in - let vars = - List.map - (function - | Ast.Variable v -> v - | _ -> assert false) - first_column - in - variable_closure21 vars (aux t'' k) - | _ -> - let pidl = - List.map - (function - | p :: _, _ -> fst (CicNotationTag.get_tag p) - | [], _ -> assert false) - t' - in - let clusters = Patterns21.partition t' pidl in - let ks = - List.map - (fun (pid, cluster) -> - let cluster' = - List.map (* add args as patterns heads *) - (function - | p :: tl, pid -> - let _, subpatterns = CicNotationTag.get_tag p in - subpatterns @ tl, pid - | _ -> assert false) - cluster - in - pid, aux cluster' k) - clusters - in - constructor_closure21 ks k) - | t', tl -> aux t' (aux tl k) + (subst pos env hd) :: subst_children pos' env tl in - let matcher = aux t (fun _ _ -> raise No_match) in - (fun ast -> - try - matcher [ast] (List.map (fun (_, pid) -> [], pid) t) - with No_match -> fail_k ast) - -let ast_of_acic1 term_info annterm = (get_compiled32 ()) term_info annterm - -let pp_ast1 term = (get_compiled21 ()) term - -let instantiate21 env pid = - prerr_endline "instantiate21"; - let precedence, associativity, l1 = - try - Hashtbl.find level1_patterns21 pid - with Not_found -> assert false + subst_singleton `Left env l1 + +let rec pp_ast1 term = + let rec pp_value = function + | CicNotationEnv.NumValue _ as v -> v + | CicNotationEnv.StringValue _ as v -> v +(* | CicNotationEnv.TermValue t when t == term -> CicNotationEnv.TermValue (pp_ast0 t pp_ast1) *) + | CicNotationEnv.TermValue t -> CicNotationEnv.TermValue (pp_ast1 t) + | CicNotationEnv.OptValue None as v -> v + | CicNotationEnv.OptValue (Some v) -> + CicNotationEnv.OptValue (Some (pp_value v)) + | CicNotationEnv.ListValue vl -> + CicNotationEnv.ListValue (List.map pp_value vl) in - let rec subst = function - | Ast.AttributedTerm (_, t) -> subst t - | Ast.Variable var -> - (try List.assoc var env with Not_found -> assert false) - | (Ast.Literal _ - | Ast.Magic _) 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 - -let instantiate32 term_info name_env term_env pid = - let symbol, args = - try - Hashtbl.find level2_patterns32 pid - with Not_found -> assert false + let ast_env_of_env env = + List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env in +(* prerr_endline ("pattern matching from 2 to 1 on term " ^ CicNotationPp.pp_term term); *) + match term with + | Ast.AttributedTerm (attrs, term') -> + Ast.AttributedTerm (attrs, pp_ast1 term') + | _ -> + (match (get_compiled21 ()) term with + | None -> pp_ast0 term pp_ast1 + | Some (env, ctors, pid) -> + let idrefs = + List.flatten (List.map CicNotationUtil.get_idrefs ctors) + in + let l1 = + try + Hashtbl.find level1_patterns21 pid + with Not_found -> assert false + in + instantiate21 idrefs (ast_env_of_env env) l1) + +let instantiate32 term_info idrefs 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.AttributedTerm (_, t) -> count_lambda t + | 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)) - in - let args' = List.map instantiate_arg args in - Ast.Appl (Ast.Symbol (symbol, 0) :: 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) + 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 - (name, (name', ast_ty_opt))) - name_env + add_lambda t (n - count_lambda t) in - let ast_env_of_term_env term_info = - List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) + let head = + let symbol = Ast.Symbol (symbol, 0) in + add_idrefs idrefs symbol 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 + if args = [] then head + else Ast.Appl (head :: List.map instantiate_arg args) + +let rec ast_of_acic1 term_info annterm = + let id_to_uris = term_info.uri in + let register_uri id uri = Hashtbl.add id_to_uris id uri in + match (get_compiled32 ()) annterm with + | None -> ast_of_acic0 term_info annterm ast_of_acic1 + | Some (env, ctors, pid) -> + let idrefs = + List.map + (fun annterm -> + let idref = CicUtil.id_of_annterm annterm in + (try + register_uri idref + (CicUtil.uri_of_term (Deannotate.deannotate_term annterm)) + with Invalid_argument _ -> ()); + idref) + ctors + in + 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 + let ast = instantiate32 term_info idrefs env' symbol args in + Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm), ast) + +let load_patterns32 t = + let t = + HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t in - let compiled32 = compiler32 t success_k fail_k in - set_compiled32 compiled32 + set_compiled32 (lazy (CicNotationMatcher.Matcher32.compiler t)) let load_patterns21 t = - let ast_env_of_env env = - List.map (fun (var, term) -> (var, pp_ast1 term)) env - in - let fail_k term = pp_ast0 term pp_ast1 in - let success_k (env, pid) = instantiate21 (ast_env_of_env env) pid in - let compiled21 = compiler21 t success_k fail_k in - set_compiled21 compiled21 + set_compiled21 (lazy (CicNotationMatcher.Matcher21.compiler t)) let ast_of_acic id_to_sort annterm = + debug_print (lazy ("ast_of_acic <- " + ^ CicPp.ppterm (Deannotate.deannotate_term annterm))); let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in let ast = ast_of_acic1 term_info annterm in + debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast)); ast, term_info.uri -let pp_ast term = pp_ast1 term +let pp_ast ast = + debug_print (lazy "pp_ast <-"); + let ast' = pp_ast1 ast in + debug_print (lazy ("pp_ast -> " ^ CicNotationPp.pp_term ast')); + ast' let fresh_id = let counter = ref ~-1 in @@ -734,29 +673,98 @@ let fresh_id = incr counter; !counter -let add_interpretation (symbol, args) appl_pattern = +let add_interpretation dsc (symbol, args) appl_pattern = let id = fresh_id () in - Hashtbl.add level2_patterns32 id (symbol, args); - pattern32_matrix := ([appl_pattern], id) :: !pattern32_matrix; + Hashtbl.add level2_patterns32 id (dsc, symbol, args, appl_pattern); + pattern32_matrix := (true, appl_pattern, id) :: !pattern32_matrix; load_patterns32 !pattern32_matrix; + (try + let ids = Hashtbl.find interpretations symbol in + ids := id :: !ids + with Not_found -> Hashtbl.add interpretations symbol (ref [id])); id -let add_pretty_printer ?precedence ?associativity l2 l1 = +let get_all_interpretations () = + List.map + (function (_, _, id) -> + let (dsc, _, _, _) = + try + Hashtbl.find level2_patterns32 id + with Not_found -> assert false + in + (id, dsc)) + !pattern32_matrix + +let get_active_interpretations () = + HExtlib.filter_map (function (true, _, id) -> Some id | _ -> None) + !pattern32_matrix + +let set_active_interpretations ids = + let pattern32_matrix' = + List.map + (function + | (_, ap, id) when List.mem id ids -> (true, ap, id) + | (_, ap, id) -> (false, ap, id)) + !pattern32_matrix + in + pattern32_matrix := pattern32_matrix'; + load_patterns32 !pattern32_matrix + +exception Interpretation_not_found +exception Pretty_printer_not_found + +let rec list_uniq = function + | [] -> [] + | h::[] -> [h] + | h1::h2::tl when h1 = h2 -> list_uniq (h2 :: tl) + | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl + +let lookup_interpretations symbol = + try + list_uniq + (List.sort Pervasives.compare + (List.map + (fun id -> + let (dsc, _, args, appl_pattern) = + try + Hashtbl.find level2_patterns32 id + with Not_found -> assert false + in + dsc, args, appl_pattern) + !(Hashtbl.find interpretations symbol))) + with Not_found -> raise Interpretation_not_found + +let fill_pos_info l1_pattern = l1_pattern +(* let rec aux toplevel pos = + function + | Ast.Layout l -> + (match l + + | Ast.Magic m -> + Ast.Box ( + | Ast.Variable _ as t -> add_pos_info pos t + | t -> t + in + aux true l1_pattern *) + +let add_pretty_printer ~precedence ~associativity l2 l1 = let id = fresh_id () in + let l1' = add_level_info precedence associativity (fill_pos_info l1) in let l2' = CicNotationUtil.strip_attributes l2 in - Hashtbl.add level1_patterns21 id (precedence, associativity, l1); - pattern21_matrix := ([l2'], id) :: !pattern21_matrix; + Hashtbl.add level1_patterns21 id l1'; + pattern21_matrix := (l2', id) :: !pattern21_matrix; load_patterns21 !pattern21_matrix; id -exception Interpretation_not_found -exception Pretty_printer_not_found - let remove_interpretation id = (try + let _, symbol, _, _ = Hashtbl.find level2_patterns32 id in + let ids = Hashtbl.find interpretations symbol in + ids := List.filter ((<>) id) !ids; Hashtbl.remove level2_patterns32 id; with Not_found -> raise Interpretation_not_found); - pattern32_matrix := List.filter (fun (_, id') -> id <> id') !pattern32_matrix; + pattern32_matrix := + List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix; load_patterns32 !pattern32_matrix let remove_pretty_printer id =