let set_compiled21 f = compiled21 := Some f
let set_compiled32 f = compiled32 := Some f
-let instantiate21 env pid =
+let instantiate21 env precedence associativity l1 =
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 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 =
(* 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
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