fact: Definition specific_meaning {T} (t : RLiteralNonConstructor T) : arg_meanings_for T -> option (normalized_of (range_of T)) := match t in RLiteralNonConstructor T return arg_meanings_for T -> option (normalized_of (range_of T)) with | Rfst _ _ => specific_meaning_apply1 (cprod _ _) (csimple _) (fun x => x) fst | Rsnd _ _ => specific_meaning_apply1 (cprod _ _) (csimple _) (fun x => x) snd | Rnth' _ => fun af => specific_meaning_apply2 cnat (clist _) (_ --> csimple _) (fun x => x) (fun n ls => List.nth' n ls (ahd (atl (atl af)))) af | Rnth _ => fun af => specific_meaning_apply2 cnat (clist _) (_ --> csimple _) (fun x => x) (fun n ls => List.nth n ls (ahd (atl (atl af)))) af | Rbeq_nat => specific_meaning_apply2 cnat cnat cbool (syntactify_bool _) Nat.eqb | Rmap A B => fun af => option_map (@syntactify_list _ _) (option_map (List.map (ahd af)) (constantOf (ahd (atl af)))) | Rfold_left A B => fun af => option_map (fun ls => let init := ahd (atl (atl af)) in let f := ahd af in List.fold_left f ls init) (constantOf (ahd (atl af))) | Rorb | Rorbr => fun af => match constantOf (ahd af), constantOf (ahd (atl af)) with | Some b, _ => Some (if b then syntactify_bool var true else ahd (atl af)) | _, Some b => Some (if b then syntactify_bool var true else ahd af) | None, None => None end | Randb | Randbr => fun af => match constantOf (ahd af), constantOf (ahd (atl af)) with | Some b, _ => Some (if b then ahd (atl af) else syntactify_bool var false) | _, Some b => Some (if b then ahd af else syntactify_bool var false) | None, None => None end | Rminusr => fun af => match constantOf (ahd af), constantOf (ahd (atl af)) with | Some n, Some n' => Some (syntactify_nat var (minusr n n')) | _, Some n' => Some (apply_n n' (fun n0 => RLiteralApp Rpred (n0 :: noargs)) (ahd af)) | _, _ => None end | Rpred => specific_meaning_apply1 cnat cnat (syntactify_nat _) pred | Rlength _ => specific_meaning_apply1 (clist _) cnat (syntactify_nat _) (@List.length _) | Rbool_rect_nodep cbool => fun af => let rtest := ahd (atl (atl af)) in let rtrue := ahd af in let rfalse := ahd (atl af) in match constantOf rtest, constantOf rtrue, constantOf rfalse with | Some b, _, _ => Some (if b then rtrue else rfalse) | None, Some true, Some true => Some (Syntactify.syntactify_bool _ true) | None, Some false, Some false => Some (Syntactify.syntactify_bool _ false) | None, Some true, Some false => Some rtest | None, Some false, Some true | None, None, _ | None, _, None => None end | Rbool_rect_nodep _ => fun af => option_map (fun b : bool => if b then ahd af else ahd (atl af)) (constantOf (ahd (atl (atl af)))) | Rlist_rect_nodep A P => fun af => option_map (fun ls => apply_meaning_helper (atl (atl (atl af))) (list_rect_nodep (ahd af) (fun x xs => ahd (atl af) x (syntactify_list xs)) ls)) (constantOf (ahd (atl (atl af)))) | Rlist_caset_nodep _ _ => fun af => option_map (fun ls => list_caset_nodep (ahd af) (fun x xs => ahd (atl af) x (syntactify_list xs)) ls) (constantOf (ahd (atl (atl af)))) | Rleb => specific_meaning_apply2 cnat cnat cbool (syntactify_bool _) Compare_dec.leb | Rcombine _ _ => specific_meaning_apply2 (clist _) (clist _) (clist _) (fun ls => syntactify_list (List.map (@syntactify_prod _ _ _) ls)) (@List.combine _ _) | Rrev _ => specific_meaning_apply1 (clist _) (csimple _) (@syntactify_list _ _) (@List.rev _) | Rup_to => specific_meaning_apply1 cnat (clist _) (fun ls => syntactify_list (List.map (@syntactify_nat _) ls)) List.up_to | Rplus => fun af => match constantOf (ahd af), constantOf (ahd (atl af)) with | Some n, Some n' => Some (syntactify_nat var (plus n n')) | Some n, _ => Some (apply_n n (fun n0 => RLiteralApp RS (n0 :: noargs)) (ahd (atl af))) | _, Some n' => Some (apply_n n' (fun n0 => RLiteralApp RS (n0 :: noargs)) (ahd af)) | None, None => None end | Rmax => specific_meaning_apply2 cnat cnat cnat (syntactify_nat _) max | Rritem_rect_nodep _ => fun af => option_map (fun v => Reflective.ritem_rect_nodep (fun x => ahd af (syntactify_rchar_expr_ascii var x)) (fun s => ahd (atl af) (syntactify_string var s)) v) (constantOf (ahd (atl (atl af)))) | Rfirst_index_default _ => fun af => match constantOf (ahd (atl af)), constantOf (ahd (atl (atl af))) with | Some v, Some ls => let f := ahd af in option_map (syntactify_nat var) (first_index_default_partial (fun a => constantOf (f a)) v ls) | _, _ => None end | Rstring_beq => specific_meaning_apply2 cstring cstring cbool (syntactify_bool _) Equality.string_beq | Rinterp_RCharExpr_ascii => fun _ => None end.
imports: Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.Semantics Fiat.Parsers.Reflective.Syntactify Fiat.Common Fiat.Common.NatFacts Fiat.Common.List.Operations