X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=8bbc22e24344819e37e7758abe8c5dc6f54f8f40;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=ddf429db6d469f36a8d1542adf30ad63f0a1fcbc;hpb=3065dd135001f868c677ee181d8a1fa3d498866a;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index ddf429db6..8bbc22e24 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -36,7 +36,7 @@ type pretty_printer_id = pattern_id type term_info = { sort: (Cic.id, Ast.sort_kind) Hashtbl.t; - uri: (Cic.id, string) Hashtbl.t; + uri: (Cic.id, UriManager.uri) Hashtbl.t; } let get_types uri = @@ -73,6 +73,17 @@ let resolve_binder = function | `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 @@ -125,32 +136,47 @@ let pp_ast0 t k = 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 (List.map k ts))) + (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 "."; k body ]) + builtin_symbol "."; right_pos (k body) ]) | Ast.Case (what, indty_opt, outty_opt, patterns) -> let outty_box = match outty_opt with | None -> [] | Some outty -> - [ builtin_symbol "["; remove_level_info (k outty); - builtin_symbol "]"; break ] + [ keyword "return"; break; remove_level_info (k outty)] in let indty_box = match indty_opt with | None -> [] - | Some (indty, href) -> [ keyword "in"; ident_w_href href indty ] + | Some (indty, href) -> [ keyword "in"; break; ident_w_href href indty ] in let match_box = - hvbox false true [ - keyword "match"; break; - hvbox false false ([ k what ] @ indty_box); break; - keyword "with" ] + 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) @@ -162,7 +188,7 @@ let pp_ast0 t k = (hvbox false true [ hbox false true [ mk_case_pattern lhs; builtin_symbol "\\Rightarrow" ]; - break; k rhs ])) + break; top_pos (k rhs) ])) patterns in let patterns'' = @@ -189,20 +215,20 @@ let pp_ast0 t k = in add_level_info Ast.simple_prec Ast.simple_assoc (hvbox false false [ - hvbox false false (outty_box @ [ match_box ]); break; + 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 "("; k bo; break; builtin_symbol ":"; k ty; - builtin_symbol ")"]) + 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; k s ]; + aux_var var; builtin_symbol "\\def"; break; top_pos (k s) ]; break; keyword "in" ]; break; k t ]) @@ -219,7 +245,7 @@ let pp_ast0 t k = let (name, body) = fst_fun in hvbox false true [ keyword "let"; keyword rec_op; name; builtin_symbol "\\def"; break; - body ] + top_pos body ] in let tl_rows = List.map @@ -297,14 +323,15 @@ 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 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 @@ -322,19 +349,19 @@ let ast_of_acic0 term_info acic k = 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 = sprintf "%s#xpointer(1/%d)" uri_str (i+1) in - register_uri id puri_str; + 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 @@ -426,14 +453,15 @@ let add_idrefs = List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) let instantiate21 idrefs env l1 = - let rec subst_singleton env = + let rec subst_singleton pos env = function Ast.AttributedTerm (attr, t) -> - Ast.AttributedTerm (attr, subst_singleton env t) - | t -> CicNotationUtil.group (subst env t) - and subst env = function + 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 -> - subst env t +(* 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 = @@ -447,16 +475,16 @@ let instantiate21 idrefs env l1 = (* following assertion should be a conditional that makes this * instantiation fail *) assert (CicNotationEnv.well_typed expected_ty value); - [ CicNotationEnv.term_of_value value ] - | Ast.Magic m -> subst_magic env m + [ 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 env l) ] - | t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ] - and subst_magic env = function + | 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 @@ -473,10 +501,11 @@ let instantiate21 idrefs env l1 = | [] -> List.rev acc | value_set :: [] -> let env = CicNotationEnv.combine rec_decls value_set in - instantiate_list (CicNotationUtil.group (subst env p) :: acc) [] + instantiate_list (CicNotationUtil.group (subst pos env p) :: acc) + [] | value_set :: tl -> let env = CicNotationEnv.combine rec_decls value_set in - let terms = subst env p in + let terms = subst pos env p in instantiate_list (CicNotationUtil.group (terms @ sep) :: acc) tl in instantiate_list [] values @@ -496,15 +525,37 @@ let instantiate21 idrefs env l1 = begin match env with | [] -> [] - | _ -> subst env p + | _ -> subst pos env p end | _ -> assert false (* impossible *) - and subst_layout env = function + and subst_layout pos env = function | Ast.Box (kind, tl) -> - Ast.Box (kind, List.concat (List.map (subst env) tl)) - | l -> CicNotationUtil.visit_layout (subst_singleton env) l + 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 pos' = + match pos with + | `Inner -> `Inner + | `Left -> `Inner +(* | `None -> assert false *) + | `Right -> `Right + in + (subst pos env hd) :: subst_children pos' env tl in - subst_singleton env l1 + subst_singleton `Left env l1 let rec pp_ast1 term = let rec pp_value = function @@ -532,13 +583,12 @@ let rec pp_ast1 term = let idrefs = List.flatten (List.map CicNotationUtil.get_idrefs ctors) in - let prec, assoc, l1 = + let l1 = try Hashtbl.find level1_patterns21 pid with Not_found -> assert false in - add_level_info prec assoc - (instantiate21 idrefs (ast_env_of_env env) l1)) + instantiate21 idrefs (ast_env_of_env env) l1) let instantiate32 term_info idrefs env symbol args = let rec instantiate_arg = function @@ -578,8 +628,7 @@ let rec ast_of_acic1 term_info annterm = let idref = CicUtil.id_of_annterm annterm in (try register_uri idref - (UriManager.string_of_uri - (CicUtil.uri_of_term (Deannotate.deannotate_term annterm))) + (CicUtil.uri_of_term (Deannotate.deannotate_term annterm)) with Invalid_argument _ -> ()); idref) ctors @@ -596,6 +645,9 @@ let rec ast_of_acic1 term_info annterm = 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 set_compiled32 (lazy (CicNotationMatcher.Matcher32.compiler t)) let load_patterns21 t = @@ -624,7 +676,7 @@ let fresh_id = let add_interpretation dsc (symbol, args) appl_pattern = let id = fresh_id () in Hashtbl.add level2_patterns32 id (dsc, symbol, args, appl_pattern); - pattern32_matrix := (appl_pattern, id) :: !pattern32_matrix; + pattern32_matrix := (true, appl_pattern, id) :: !pattern32_matrix; load_patterns32 !pattern32_matrix; (try let ids = Hashtbl.find interpretations symbol in @@ -632,6 +684,32 @@ let add_interpretation dsc (symbol, args) appl_pattern = with Not_found -> Hashtbl.add interpretations symbol (ref [id])); id +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 @@ -656,10 +734,24 @@ let lookup_interpretations symbol = !(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); + Hashtbl.add level1_patterns21 id l1'; pattern21_matrix := (l2', id) :: !pattern21_matrix; load_patterns21 !pattern21_matrix; id @@ -671,7 +763,8 @@ let remove_interpretation id = 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 =