From: Luca Padovani Date: Tue, 7 Jun 2005 18:24:59 +0000 (+0000) Subject: * generate list elements in correct order X-Git-Tag: PRE_INDEX_1~46 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=345d5606c989f46d9de3d3b4c6c53902fabac5bd;p=helm.git * generate list elements in correct order * handle list inside boxes * handle box layout * generate separator between elements (not after elements) --- diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 79316319a..529353daa 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -223,8 +223,14 @@ let set_compiled32 f = compiled32 := Some f let instantiate21 env precedence associativity l1 = prerr_endline "instantiate21"; - let rec subst last_box env = function - | Ast.AttributedTerm (_, t) -> subst last_box env t + let boxify = function + | [t] -> t + | tl -> Ast.Layout (Ast.Box (Ast.H, tl)) + in + let rec subst_singleton env t = + 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 = @@ -236,12 +242,12 @@ let instantiate21 env precedence associativity 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 last_box env m - | Ast.Literal _ as t -> t - | 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 + [ 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 @@ -256,12 +262,14 @@ let instantiate21 env precedence associativity l1 = in let rec instantiate_list acc = function | [] -> List.rev acc + | value_set :: [] -> + let env = CicNotationEnv.combine rec_decls value_set in + instantiate_list ((boxify (subst env p)) :: acc) [] | value_set :: tl -> let env = CicNotationEnv.combine rec_decls value_set in - instantiate_list ([subst last_box env p] @ sep @ acc) tl + instantiate_list ((boxify (subst env p @ sep)) :: acc) tl in - let children = instantiate_list [] values in - CicNotationPt.Layout (CicNotationPt.Box (last_box, children)) + instantiate_list [] (List.rev values) | Ast.Opt p -> let opt_decls = CicNotationEnv.declarations_of_term p in let env = @@ -275,18 +283,17 @@ let instantiate21 env precedence associativity l1 = 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)) + begin + match env with + | [] -> [] + | _ -> subst env p + end | _ -> 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 :-((( *) + 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 CicNotationPt.H env l1 + subst_singleton env l1 let rec pp_ast1 term = let rec pp_value = function