X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=2f95a56350f5af1b5fa492c36d2310fa18debb18;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=2e2d8c9d45f3699180658824d40b00939c5bb66a;hpb=bf6144a808a16d4e576e56593bbcd63b8db5fe4c;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 2e2d8c9d4..2f95a5635 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -62,6 +62,7 @@ let constructor_of_inductive_type uri i j = with Not_found -> assert false) module Ast = CicNotationPt +module Parser = CicNotationParser let string_of_name = function | Cic.Name s -> s @@ -71,11 +72,41 @@ 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 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 -> + Ast.AttributedTerm (`Level (Parser.apply_prec, Parser.apply_assoc), + Ast.Layout (Ast.Box ((Ast.HOV, true, true), List.map k ts))) + | Ast.Binder (`Forall, (Ast.Ident ("_", _), ty), body) + | Ast.Binder (`Pi, (Ast.Ident ("_", _), ty), body) -> + Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc), + Ast.Layout (Ast.Box ((Ast.HV, false, true), [ + aux_ty ty; + Ast.Layout (Ast.Box ((Ast.H, false, false), [ + Ast.Literal (`Symbol "\\to"); k body]))]))) + | Ast.Binder (binder_kind, (id, ty), body) -> + Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc), + Ast.Layout (Ast.Box ((Ast.HV, false, true), [ + Ast.Layout (Ast.Box ((Ast.H, false, false), [ + Ast.Literal (`Symbol (resolve_binder binder_kind)); + k id; + Ast.Literal (`Symbol ":"); + aux_ty ty ])); + Ast.Layout (Ast.Box ((Ast.H, false, false), [ + Ast.Literal (`Symbol "."); + k body ]))]))) + | t -> CicNotationUtil.visit_ast ~special_k k t + and aux_ty = function + | None -> Ast.Literal (`Symbol "?") + | Some ty -> k ty and special_k = function - | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, aux t) + | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t) | _ -> assert false in aux t @@ -221,15 +252,11 @@ let get_compiled32 () = let set_compiled21 f = compiled21 := Some f let set_compiled32 f = compiled32 := Some f -let instantiate21 env pid = - 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 instantiate21 env precedence associativity l1 = + let rec subst_singleton env t = + CicNotationUtil.boxify (subst env t) + and subst env = function + | Ast.AttributedTerm (_, t) -> subst env t | Ast.Variable var -> let name, expected_ty = CicNotationEnv.declaration_of_var var in let ty, value = @@ -241,13 +268,60 @@ let instantiate21 env pid = (* 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 _ -> assert false (* TO BE IMPLEMENTED *) - | 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 + [ CicNotationEnv.term_of_value value ] + | Ast.Magic m -> subst_magic env m + | Ast.Literal _ as 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.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 :: [] -> + let env = CicNotationEnv.combine rec_decls value_set in + instantiate_list + ((CicNotationUtil.boxify (subst env p)) :: acc) [] + | value_set :: tl -> + let env = CicNotationEnv.combine rec_decls value_set in + instantiate_list + ((CicNotationUtil.boxify (subst env p @ 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 env p + end + | _ -> assert false (* impossible *) + and subst_layout env = function + | Ast.Box (kind, tl) -> Ast.Box (kind, List.concat (List.map (subst env) tl)) + | l -> CicNotationUtil.visit_layout (subst_singleton env) l + in + subst_singleton env l1 let rec pp_ast1 term = let rec pp_value = function @@ -265,7 +339,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